#!/bin/bash

SCRIPT_DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" && pwd )"

FSM=
NSTATES=
NLTL=
NEVENTS=
MIN_ACTIONS=
NACTIONS=
ACTIONS_SEQ_LEN=
NVARIABLES=
TRANSITION_PERCENT=
LTLPRIORITIES=

#the number of initially generated LTL formulae is NSTATES * MULT
MULT=200

# N_CHECK_REPEATS is the number of random EFSMs used to check a particular LTL formula.
# When a formula candidate is examined, N_CHECK_REPEATS random EFSMs are generated. 
# The formula is verified for each of these EFSMs.
# If less than THRESHOLD percent of these EFSMs satisfy the formula, the formula is accepted.
if [[ -z $N_CHECK_REPEATS ]]
then
    N_CHECK_REPEATS=10
fi

if [[ -z $THRESHOLD ]]
then
    THRESHOLD=50
fi

if [[ -z $TREE_SIZE ]]
then
     TREE_SIZE=15
fi


while getopts ':m:n:f:h:e:i:a:s:v:x:p:u:' opt ; do
    case "$opt" in
        m) FSM="$OPTARG" ;;
        n) NSTATES="$OPTARG" ;;
        f) NLTL="$OPTARG" ;;
        h) THRESHOLD="$OPTARG" ;; 
        e) NEVENTS="$OPTARG" ;;
        i) MIN_ACTIONS="$OPTARG" ;;
        a) NACTIONS="$OPTARG" ;;
        s) ACTIONS_SEQ_LEN="$OPTARG" ;;
        v) NVARIABLES="$OPTARG" ;; 
        x) MULT="$OPTARG" ;;
        p) TRANSITION_PERCENT="$OPTARG" ;;
        u) LTLPRIORITIES="$OPTARG" ;;
        [?]) echo >&2 "Usage: $0 -m (EFSM file in graphviz format) -n (desired number of EFSM states) -f (number of desired LTL formulae) -h (threshold, default = 50) -e (number of events) -i (min number of actions) -a (max number of actions) -s (max action sequence length) -v (number of internal variables) -t (percentage of generated transitions) -u (LTL priorities in the randltl format)" && exit 1 ;;
    esac
done

if [[ -z $FSM || -z $NSTATES || -z $NLTL || -z $TREE_SIZE || -z $THRESHOLD || -z $NEVENTS || -z $MIN_ACTIONS || -z $NACTIONS || -z $ACTIONS_SEQ_LEN || -z $NVARIABLES || -z $TRANSITION_PERCENT ]]
then 
    echo >&2 "Usage: $0 -m (EFSM file) -n (number of EFSM states) -f (desired number of LTL formulae) -h (threshold) -e (number of events) -i (min number of actions) -a (max number of actions) -s (max action sequence length) -v (number of internal variables) -t (percentage of generated transitions)"
    exit 1 
fi

fsmdir=$(pwd)
root="$fsmdir/$(mktemp -d)"
mkdir -p $root
cd $root

n_generate_ltl=$(expr $NLTL \* $MULT)

TREE_SIZE=$TREE_SIZE $SCRIPT_DIR/prepare-formulas -a $fsmdir/$FSM -n $NSTATES -f $n_generate_ltl -u "$LTLPRIORITIES" > selected-formulas
echo "    Prepared $(cat selected-formulas | wc -l) formulas, checking"

cat selected-formulas | split -l 1 -d 

for ltl_file in $(ls x*) ; do
    echo "        Checking formula $ltl_file [ $(cat $ltl_file) ]"
    workdir="$root/tmp/$ltlfile"
    mkdir -p $workdir
    cnt=0
    for (( j=0; j < $N_CHECK_REPEATS; j+=1)) ; do
        checkwd=$workdir/$j
        #$(mktemp -d)
        mkdir -p $checkwd
        java -jar $SCRIPT_DIR/../jars/automaton-generator.jar -s $NSTATES -ec $NEVENTS -mina $MIN_ACTIONS -ac $NACTIONS -maxa $ACTIONS_SEQ_LEN -vc $NVARIABLES -p $TRANSITION_PERCENT -o $checkwd/efsm.gv
        $SCRIPT_DIR/select-formulas -a $checkwd/efsm.gv -n $NSTATES -f "$root/$ltl_file" > $checkwd/true_formulas
        cnt=$(expr $cnt + $(wc -l $checkwd/true_formulas | awk '{print $1}'))
    done
    ratio=$(echo "scale=0; 100 * $cnt / $N_CHECK_REPEATS" | bc)
    if [[ "$ratio" -le "$THRESHOLD" ]]
    then
        cat $ltl_file >> $fsmdir/formulae
        echo "        $ltl_file : $cnt/$N_CHECK_REPEATS EFSMs satisfy the formula, ACCEPT"
    else
        echo "        $ltl_file : $cnt/$N_CHECK_REPEATS EFSMs satisfy the formula, REJECT"
    fi
    
    if [[ -f "$fsmdir/formulae" ]]
    then
        nprepared_formulas=$(cat $fsmdir/formulae | wc -l)
        if [[ "$nprepared_formulas" -ge "$NLTL" ]]
        then 
            rm -rf $fsmdir/tmp
            exit 0
        fi
    fi
done
cd $fsmdir
rm -rf $fsmdir/tmp
